ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A,B:ecl-trans-tuple{i:l}(ds; da),
f:(()()), g:(), L:(event-info(ds;da) List).
(L':(event-info(ds;da) List). 
iseg(event-info(ds;da); L'; L)  ((ecl-trans-h(A)(0,ecl-trans-state(A; L'))))  (L' = L))
 (ecl-trans-state(combine-ecl-tuples(A; B; f; g); L)
 (=
 (<ecl-trans-state(A; L), ecl-trans-state(B; [])>
 ( ecl-trans-type(combine-ecl-tuples(A; B; f; g))) 

latex

Definitions

Id, fpf(A; a.B(a)), Knd, , x. t(x), guard(T), append(as; bs), iseg(T; l1; l2), b, ecl-trans-h(v), prop{i:l}, , A, False, P  Q, A  B, subtype(S; T), ecl-trans-state(v; L), event-info(ds;da), ecl-trans-tuple{i:l}(ds; da), combine-ecl-tuples(A; B; f; g), ecl-trans-type(A), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), x:A. B(x), t  T, ecl-trans-init(v), ecl-trans-state-from(v; z; L), top, P  Q, P  Q, T, band(p; q), True, bor(p; q), Unit, deq-member(eq; x; L), b, Kind-deq, ma-valtype(da; k), P  Q, P  Q, (x  l)

Lemmas

l member wf, member append, not wf, Kind-deq wf, bnot wf, deq-member wf, assert-deq-member, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, bor wf, band wf, or functionality wrt iff, assert of bor, bnot thru band, true wf, squash wf, and functionality wrt iff, assert of band, iseg append0, append-impossible, ecl-trans-state-from wf, ecl-trans-state-append, top wf, length-append, iseg length, iseg append, subtype rel self, event-info wf, ecl-trans-state wf, le wf, combine-ecl-tuples wf, ecl-trans-type wf, ecl-trans-h wf, assert wf, iseg wf, append wf, last induction, bool wf, nat wf, ecl-trans-tuple wf, Knd wf, fpf wf, Id wf